L:(Realizer List), A:Realizer. (BL.A  B)  A  (L) 

latex

Definitions	P & Q, x. t(x), t  T, , P  Q, P  Q, P  Q, Y, reduce(f;k;as), (L), P  Q, x:A. B(x), False, {T}, x(s)
Lemmas	R-sub-plus-right, R-sub-plus-left, R-sub transitivity, l exists nil, false wf, es realizer wf, l exists cons, implies functionality wrt iff, Rlist wf, Rplus wf, R-sub wf, l exists wf, all functionality wrt iff